// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
package org.kframework.backend.kore;

import org.kframework.attributes.Att;
import org.kframework.builtin.KLabels;
import org.kframework.definition.Module;
import org.kframework.definition.Production;
import org.kframework.kore.FoldK;
import org.kframework.kore.K;
import org.kframework.kore.KApply;
import org.kframework.kore.KAs;
import org.kframework.kore.KLabel;
import org.kframework.utils.errorsystem.KException;
import scala.collection.Set;

public class ConstructorChecks {
  private final Module module;

  public ConstructorChecks(Module m) {
    module = m;
  }

  /**
   * Checks whether a lhs pattern is constructor-based, i.e., an application of a function symbol to
   * a list of constructor terms.
   *
   * @param term
   * @return
   */
  public boolean isConstructorBased(K term) {
    if (term instanceof KApply) {
      return ((KApply) term).klist().items().stream().allMatch(this::isConstructorTerm);
    }
    if (term instanceof KAs) {
      return isConstructorBased(((KAs) term).pattern());
    }
    KException.criticalError("Unexpecting isConstructorBased call on " + term.getClass());
    return false;
  }

  /**
   * Checks whether a pattern is a constructor term, i.e., it is not formed by means of reducible
   * symbols (functions).
   *
   * @param term
   * @return
   */
  public boolean isConstructorTerm(K term) {
    return (new FoldK<Boolean>() {
          @Override
          public Boolean unit() {
            return true;
          }

          @Override
          public Boolean merge(Boolean a, Boolean b) {
            return a && b;
          }

          @Override
          public Boolean apply(KApply k) {
            return isConstructorLike(k.klabel()) && super.apply(k);
          }
        })
        .apply(term);
  }

  // the functions below could be moved to a common place and made public

  private boolean isConstructorLike(KLabel klabel) {
    String labelName = klabel.name();
    if (isBuiltinLabel(klabel)) return false;
    if (isInjectionLabel(labelName) || isBuiltinModuloConstructor(klabel)) return true;
    Set<Production> productionSet = module.productionsFor().apply(klabel.head());
    assert productionSet.size() == 1 : "Should not have more than one production";
    Production production = productionSet.head();
    return !production.att().contains(Att.FUNCTION());
  }

  public static boolean isBuiltinLabel(KLabel label) {
    return label.name().equals(KLabels.ML_FALSE.name())
        || label.name().equals(KLabels.ML_TRUE.name())
        || label.name().equals(KLabels.ML_NOT.name())
        || label.name().equals(KLabels.ML_OR.name())
        || label.name().equals(KLabels.ML_AND.name())
        || label.name().equals(KLabels.ML_IMPLIES.name())
        || label.name().equals(KLabels.ML_EQUALS.name())
        || label.name().equals(KLabels.ML_CEIL.name())
        || label.name().equals(KLabels.ML_FLOOR.name())
        || label.name().equals(KLabels.ML_EXISTS.name())
        || label.name().equals(KLabels.ML_FORALL.name())
        || label.name().equals(KLabels.CTL_AG.name())
        || label.name().equals(KLabels.RL_wEF.name())
        || label.name().equals(KLabels.RL_wAF.name());
  }

  private boolean isBuiltinModuloConstructor(KLabel label) {
    return label.equals(KLabels.DotMap)
        || label.equals(KLabels.Map)
        || label.equals(KLabels.MapItem)
        || label.equals(KLabels.DotList)
        || label.equals(KLabels.List)
        || label.equals(KLabels.ListItem)
        || label.equals(KLabels.DotSet)
        || label.equals(KLabels.Set)
        || label.equals(KLabels.SetItem);
  }

  private boolean isInjectionLabel(String labelName) {
    return labelName.equals(KLabels.INJ);
  }
}
